The controller enables the robot to perform smooth and natural skateboarding motions, with reliable mode identification and transitions under disturbances. Abstract --This paper introduces Discrete-time Hybrid Automata Learning (DHAL), a framework using on-policy Reinforcement Learning to identify and execute mode-switching without trajectory segmentation or event function learning. Hybrid dynamical systems, which include continuous flow and discrete mode switching, can model robotics tasks like legged robot locomotion. Model-based methods usually depend on predefined gaits, while model-free approaches lack explicit mode-switching knowledge. Current methods identify discrete modes via segmentation before regressing continuous flow, but learning high-dimensional complex rigid body dynamics without trajectory labels or segmentation is a challenging open problem. Our approach incorporates a beta policy distribution and a multi-critic architecture to model contact-guided motions, exemplified by a challenging quadrupedal robot skateboard task. I. INTRODUCTION Legged robots are often regarded as the ideal embodiment of robotic systems, designed to perform a wide range of tasks and navigate diverse destinations. Many of these tasks, such as skateboarding and boxing, are inherently contact-guided, involving complex sequences of contact events [1]. Designing and executing such contact-guided control is highly non-trivial due to two major challenges: (1) the hybrid dynamics system problem arising from the abrupt transitions introduced by contact events [2], and (2) the sparsity of contact events, which poses significant difficulties for both model-based and model-free control strategies. In model-based control, Hybrid Automata has been proposed as a powerful framework to model systems with both discrete and continuous dynamics [3, 4]. This framework has been widely applied to behavior planning [5] and legged locomotion. However, due to the combinatorial nature of hybrid dynamics, finding optimal policies for hybrid systems through model-based optimization is computationally challenging, especially for tasks with high-dimensional state and action spaces. Model-free RL requires minimal assumptions and can be applied to a diverse range of tasks across different dynamic systems [6, 7]. However, RL policies, often represented by deep neural networks, lack interpretability and fail to explicitly model hybrid dynamics [8].

Verifying the correct behavior of robots in contact tasks is challenging due to model uncertainties associated with contacts. Standard methods for testing often fall short since all (uncountable many) solutions cannot be obtained. Instead, we propose to formally and efficiently verify robot behaviors in contact tasks using reachability analysis, which enables checking all the reachable states against user-provided specifications. To this end, we extend the state of the art in reachability analysis for hybrid (mixed discrete and continuous) dynamics subject to discrete-time input trajectories. In particular, we present a novel and scalable guard intersection approach to reliably compute the complex behavior caused by contacts. We model robots subject to contacts as hybrid automata in which crucial time delays are included. The usefulness of our approach is demonstrated by verifying safe human-robot interaction in the presence of constrained collisions, which was out of reach for existing methods.

We present a novel method for the safety verification of nonlinear dynamical models that uses neural networks to represent abstractions of their dynamics. Neural networks have extensively been used before as approximators; in this work, we make a step further and use them for the first time as abstractions. For a given dynamical model, our method synthesises a neural network that overapproximates its dynamics by ensuring an arbitrarily tight, formally certified bound on the approximation error. For this purpose, we employ a counterexample-guided inductive synthesis procedure. We show that this produces a neural ODE with non-deterministic disturbances that constitutes a formal abstraction of the concrete model under analysis. This guarantees a fundamental property: if the abstract model is safe, i.e., free from any initialised trajectory that reaches an undesirable state, then the concrete model is also safe. By using neural ODEs with ReLU activation functions as abstractions, we cast the safety verification problem for nonlinear dynamical models into that of hybrid automata with affine dynamics, which we verify using SpaceEx. We demonstrate that our approach performs comparably to the mature tool Flow* on existing benchmark nonlinear models. We additionally demonstrate and that it is effective on models that do not exhibit local Lipschitz continuity, which are out of reach to the existing technologies.

The ability to model continuous change in Reiter's temporal situation calculus action theories has attracted a lot of interest. In this paper, we propose a new development of his approach, which is directly inspired by hybrid systems in control theory. Specifically, while keeping the foundations of Reiter's axiomatization, we propose an elegant extension of his approach by adding a time argument to all fluents that represent continuous change. Thereby, we insure that change can happen not only because of actions, but also due to the passage of time. We present a systematic methodology to derive, from simple premises, a new group of axioms which specify how continuous fluents change over time within a situation. We study regression for our new temporal basic action theories and demonstrate what reasoning problems can be solved. Finally, we formally show that our temporal basic action theories indeed capture hybrid automata.

Many practical applications (e.g., plannning for cyber-physical systems) require reasoning about hybrid domains that contain both probabilistic and nondeterministic parametric uncertainty. In general, this is an undecidable problem. We use delta-satisfiability to sidestep undecidability, and we develop an algorithm that computes an enclosure for the range of probability of reaching a goal region in a given number of discrete steps. We utilize SMT techniques that enable reasoning in a safe way, i.e., the computed enclosure is formally guaranteed to contain the reachability probability. We demonstrate the usefulness of our technique on challenging nonlinear hybrid domains.

Hybrid planning with nonlinear continuous change is a significant challenge for existing planners. Prior works limit their scope to linear change or base their formalisms in model checking frameworkswith inherent limitations. We address nonlinear PDDL+ planning with anew encoding in first order logic over real valued functions. Our planner, PluReal, translates PDDL+ to this logical encoding and applies the dReal Satisfiability Modulo Theories (SMT) solver to construct plans. Unlike prior work that uses dReal in the hybrid system model checking tradition, PluReal is based in the planning as satisfiability (SAT) heritage. Adopting the SAT approach helps lift several unnatural restrictions that are imposed by the translation through hybrid systems and leads to improved scalability even without SMT solver variable selection heuristics.

Planning in hybrid domains is an important and challenging task, and various planning algorithms have been proposed in the last years. From an abstract point of view, hybrid planning domains are based on hybrid automata, which have been studied intensively in the model checking community. In particular, powerful model checking algorithms and tools have emerged for this formalism. However, despite the quest for more scalable planning approaches, model checking algorithms have not been applied to planning in hybrid domains so far. In this paper, we make a first step in bridging the gap between these two worlds. We provide a formal translation scheme from PDDL+ to the standard formalism of hybrid automata, as a solid basis for using hybrid system model-checking tools for dealing with hybrid planning domains. As a case study, we use the SpaceEx model checker, showing how we can address PDDL+ domains that are out of the scope of state-of-the-art planners.

Hybrid automata networks (HAN) are a powerful formalism to model complex embedded systems. In this paper, we survey the recent advances in the application of Satisfiability Modulo Theories (SMT) to the analysis of HAN. SMT can be seen as an extended form of Boolean satisfiability (SAT), where literals are interpreted with respect to a background theory (e.g. linear arithmetic). HAN can be symbolically represented by means of SMT formulae, and analyzed by generalizing to the case of SMT the traditional model checking algorithms based on SAT.

In this paper we present pddl+, a planning domain description language for modelling mixed discrete-continuous planning domains. We describe the syntax and modelling style of pddl+, showing that the language makes convenient the modelling of complex time-dependent effects. We provide a formal semantics for pddl+ by mapping planning instances into constructs of hybrid automata. Using the syntax of HAs as our semantic model we construct a semantic mapping to labelled transition systems to complete the formal interpretation of pddl+ planning instances. An advantage of building a mapping from pddl+ to HA theory is that it forms a bridge between the Planning and Real Time Systems research communities. One consequence is that we can expect to make use of some of the theoretical properties of HAs. For example, for a restricted class of HAs the Reachability problem (which is equivalent to Plan Existence) is decidable. pddl+ provides an alternative to the continuous durative action model of pddl2.1, adding a more flexible and robust model of time-dependent behaviour.